i:Id, X, T:Type, x0:X, P:(XTProp).
Normal(T)
 Normal(X)
 (x:X. Dec(v:T. P(x,v)))
 R-Feasible(preinit1R{x:ut2, a:ut2}
 R-Feasible(preinit1R(i; X; T; x0; P)) 

latex

Definitions

Raframe-k(x1), P  Q, t  T, Rbframe-k(x1), (x,yL.P(x;y)), IdDeq, tl(l), R-Feasible(R), b, Rsends-ds(x1), {T}, Rsends?(x1), True, Rbframe-L(x1), Rsends-g(x1), Rpre?(x1), p  q, Rsends-dt(x1), Rplus-left(x1), R-interface-compat(A;B), A & B, Reffect?(x1), Reffect-x(x1), Rsframe?(x1), SQType(T), Reffect-ds(x1), Rrframe-L(x1), false, P & Q, ij, Rsends-l(x1), i<j, 2of(t), x:A. B(x), nth_tl(n;as), Rda(R), Rsframe-tag(x1), Rframe-x(x1), Rplus-right(x1), Rrframe?(x1), if b t else f fi, Reffect-knd(x1), true, Rsends-T(x1), Raframe?(x1), R-base-domain(R), l[i], i=j, xL. P(x), x:A. B(x), hd(l), Rsframe-L(x1), Rbframe?(x1), Rpre-a(x1), Rrframe-x(x1), Top, Reffect-T(x1), A || B, s.x, x. t(x), 1of(t), Rframe?(x1), preinit1R{$x:ut2, $a:ut2}(i; X; T; x0; P), Y, Rds(R), R-frame-compat(A;B), Rsframe-lnk(x1), R-loc(R), Raframe-L(x1), "$x", Prop, ||as||, Atom2Deq, Rsends-knd(x1), a = b, p = q, Rpre-ds(x1), eq_atom$n(x;y), Rplus?(x1), eqof(d), Rframe-L(x1), Rnone?(x1), {i..j}, Dec(P), (x  l), x(s), Id, , Unit, , Realizer, State(ds), Normal(T), P  Q, P  Q,

Lemmas

R-feasible-Rlist, Rpre wf, eqff to assert, subtype rel self, assert-eq-id, eqof eq btrue, fpf-cap-single, assert wf, iff transitivity, assert of bnot, normal-ds-single, eq id wf, fpf-empty-compatible-right, top wf, bnot wf, locl wf, Knd wf, normal-type wf, Rinit wf, int seg wf, not wf, id-deq wf, not functionality wrt iff, R-Feasible wf, fpf-compatible-self, eqtt to assert, decidable wf, fpf-single wf, l member wf, decidable int equal, Kind-deq wf, bool wf, Id wf